A, B:Realizer. A || B  B || A 

latex

Definitions

x:A. B(x), P  Q, A || B, t  T, Prop, Y, if b t else f fi, P & Q, True, true, false, x. t(x), AB, A, False, ij, , , Unit, P  Q, P  Q, {T}, x(s), ,

Lemmas

nat wf, R-size wf, nat plus wf, R-compat wf, es realizer wf, le wf, Rplus? wf, bool wf, eqtt to assert, R-size-decreases, Rplus-implies, R-compat-Rplus2, Rplus-left wf, Rplus-right wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Rnone? wf, true wf, eq id wf, R-loc wf, Id wf, assert-eq-id, eq bd wf, R-base-domain wf, fpf-compatible-symmetry, fpf-compatible wf, id-deq wf, Rds wf, Knd wf, Kind-deq wf, Rda wf, not functionality wrt iff, base-domain-type wf, assert-eq-bd, R-frame-compat wf, R-interface-compat wf, nat properties, ge wf